Nuprl Lemma : increasing_is_id
11,40
postcript
pdf
k
:
,
f
:({0..
k
}
{0..
k
}). increasing(
f
;
k
)
(
i
:{0..
k
}.
f
(
i
) =
i
)
latex
Definitions
i
j
,
False
,
A
,
A
B
,
suptype(
S
;
T
)
,
S
T
,
t
T
,
P
Q
,
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
i
j
<
k
,
{
i
..
j
}
,
increasing(
f
;
k
)
,
,
{
T
}
,
SQType(
T
)
,
P
Q
,
Dec(
P
)
Lemmas
ge
wf
,
nat
properties
,
le
wf
,
increasing
wf
,
int
seg
wf
,
nat
wf
,
increasing
implies
,
decidable
int
equal
origin
k:
, f:({0..k
}
{0..k}). increasing(f;k) 
(i:{0..k}. f(i) = i 
) k:, f:({0..k}{0..k}). increasing(f;k) (i:{0..k}. f(i) = i ) 
j 
A
B
T T Qx:A. B(x) j < k}
Q